
{
  open Lexing
  open Parser

  (* Used to count keywords *)
  let counts = Hashtbl.create 70

  (* Lexical errors *)
  exception Lexical_error of string

  (* Identifiers and Murphi keywords *)
  let id_or_keyword =
    let h = Hashtbl.create 70 in
    List.iter (fun (s, k) -> Hashtbl.add h s k)
      [ "alias", ALIAS; "array", ARRAY; "assert", ASSERT; "begin", BEGIN;
        (*"boolean", BOOLEAN;*) "by", BY; "case", CASE; "choose", CHOOSE; (* new keyword *)
        "clear", CLEAR; (* should use undefine instead (mainly for scalarset / unions) *)
        "const", CONST; "do", DO; "else", ELSE; "elsif", ELSIF; "end", END;
        "endalias", ENDALIAS; (* not in doc *) "endchoose", ENDCHOOSE; (* used in current murphi but not in doc *)
        "endexists", ENDEXISTS; "endfor", ENDFOR; "endforall", ENDFORALL;
        "endfunction", ENDFUNCTION; (* not in doc *) "endif", ENDIF;
        "endprocedure", ENDPROCEDURE; (* not in doc *) "endrecord", ENDRECORD; (* not in doc *)
        "endrule", ENDRULE; (* not in doc *) "endruleset", ENDRULESET; (* not in doc *)
        "endstartstate", ENDSTARTSTATE;	(* not in doc *) "endswitch", ENDSWITCH;
        "endwhile", ENDWHILE; (* not in doc *) "enum", ENUM; "error", ERROR;
        "exists", EXISTS; (*"false", FALSE;*) "for", FOR; "forall", FORALL;
        "function", FUNCTION; "if", IF; "in", IN; (* future use *)
        "interleaved", INTERLEAVED; (* future use *) "invariant", INVARIANT;
        "ismember", ISMEMBER; (* new keyword *) "isundefined", ISUNDEFINED; (* new keyword *)
        "multiset", MULTISET; (* new type *) "multisetadd", MULTISETADD; (* new keyword *)
        "multisetcount", MULTISETCOUNT;	(* new keyword *) "multisetremove", MULTISETREMOVE; (* new keyword *)
        "multisetremovepred", MULTISETREMOVEPRED; (* new keyword *) "of", OF;
        "procedure", PROCEDURE; "process", PROCESS; (* future use *)
        "program", PROGRAM; (* future use *) "put", PUT; "record", RECORD;
        "return", RETURN; "rule", RULE; "ruleset", RULESET;
        "scalarset", SCALARSET;	(* new type *) "startstate", STARTSTATE;
        "switch", SWITCH; "then", THEN; "to", TO; "traceuntil", TRACEUNTIL; (* future use *)
        (*"true", TRUE;*) "type", TYPE; "undefine", UNDEFINE; (* new keyword *)
        "undefined", UNDEFINED;	(* used in current murphi but not found in doc *)
        "union", UNION; (* new type *) "var", VAR; "while", WHILE ];
(*    fun s -> try Hashtbl.find h s with Not_found -> ID s *)
    fun s ->
	try
            let kw = (String.lowercase s) in
	    let t = Hashtbl.find h kw in
            begin try
                let c = Hashtbl.find counts kw in
	        Hashtbl.replace counts kw (c + 1)
            with Not_found -> Hashtbl.replace counts kw 1 end;
            t
	with Not_found -> ID s

  (* Prints the keywords that were used *)
  let print_used_keywords () =
    let lst = Hashtbl.fold (fun k v acc -> (k, v) :: acc) counts [] in
    let sort_asc = fun (sa, ca) (sb, cb) ->
        if (ca < cb) then -1
        else if (ca > cb) then 1
        else 0
    in
    let sort_dsc = fun (sa, ca) (sb, cb) ->
        if (ca > cb) then -1
        else if (ca < cb) then 1
        else 0
    in
    let lst = List.sort sort_dsc lst in
    Printf.printf "Different keywords : %d\n" (List.length lst);
    let f = (fun (s, c) -> Printf.printf "%d %s\n" c s) in
    List.iter f lst;
    Printf.printf "End of keywords\n"

  (* Newline handling *)
  let newline lexbuf =
    let pos = lexbuf.lex_curr_p in
    lexbuf.lex_curr_p <-
      { pos with
          pos_lnum = pos.pos_lnum + 1;
          pos_bol = pos.pos_cnum;
          pos_cnum = 0 }
}

let letter = ['a'-'z' 'A'-'Z' '_']
let digit = ['0'-'9']
let ident = letter (letter | digit)*
let str = '"' [^ '"' '\n']* '"'

rule token = parse
| "--" [^'\n']* ('\n' | eof) { newline lexbuf; token lexbuf }
| "/*"			{ comment lexbuf; token lexbuf }
| '\n'			{ newline lexbuf; token lexbuf }
| [' ' '\t' '\r']	{ token lexbuf }
| ".."			{ DOTDOT }
| "==>"			{ LONGARROW }
| "->"			{ IMPLIES }
| ":="			{ ASSIGN }
| '.'			{ DOT }
| ','			{ COMMA }
| ';'			{ SC }
| '{'			{ LCB }
| '}'			{ RCB }
| '['			{ LSB }
| ']'			{ RSB }
| '('			{ LP }
| ')'			{ RP }
| '&'			{ AND }
| '|'			{ OR }
| '!'			{ NOT }
| '?'			{ QM }
| ':'			{ COL }
| '='			{ EQ }
| "!="			{ NEQ }
| "<="			{ LEQ }
| ">="			{ GEQ }
| '<'			{ LT }
| '>'			{ GT }
| '+'			{ PLUS }
| '-'			{ MINUS }
| '*'			{ TIMES }
| '/'			{ DIV }
| '%'			{ MOD }
| ident	as s		{ id_or_keyword s }
| str	as s		{ STRING (s) }
| digit+ as s
  {
    try INTCONST (Int32.of_string s)
    with _ -> raise (Lexical_error ("Invalid integer constant : '" ^ s ^ "'"))
  }
| eof			{ print_used_keywords (); EOF }
| _			{ raise (Lexical_error ("Illegal character : " ^ lexeme lexbuf)) }

(* Multi-line comment handling *)
and comment = parse
| "*/" { () }
| '\n' { newline lexbuf; comment lexbuf }
| eof  { raise (Lexical_error "Unterminated comment") }
| _    { comment lexbuf }

